(DEFPROP TRANSF (
 TRANSFORM
 TRANSA
 TRANSB1
 TRANSB2
 SIDE
 INST
 ISVAR
)TRANSFFNS)


;;;Espression simplifier and two versions of rule application and rules.


;;;apply a list of xformation rules R to an expression E.  
;;;DONE is a list of expressions knowm to be completely xformed.
;;;Go through the list of rules (TRANSA) and apply the first applicable rule (TRANSB)
;;;	If a transformation is found the restart with result as new E.
;;;	If not work on car and cdr.  
;;;	If any change results begin again on the cons of the xformed car and cdr.

(DEFUN TRANSFORM (E R DONE) 
  (COND ((MEMBER E DONE) E)
	(T ((LAMBDA (W) 
	      (COND ((EQ W E)
		     (COND ((ATOM E) E)
			    (T ((LAMBDA (X Y) 
				   (COND ((AND (EQ X (CAR E)) (EQ Y (CDR E)))
					  (SIDE E (SETQ DONE (CONS E DONE))))
					 (T (TRANSFORM (CONS X Y) R DONE)) ))
		                 (TRANSFORM (CAR E) R DONE)
			         (TRANSFORM (CDR E) R DONE)) )))
		    (T (TRANSFORM W R DONE)) ))
	    (TRANSA E R))) ))

(DEFUN TRANSA (E R) 
  (COND ((NULL R) E)
	(T ((LAMBDA (W) (COND ((EQ W E) (TRANSA E (CDR R)))
			      (T W)))
	    (TRANSB E (CAR R)))) ))

;;;TRANSB attempts to  apply a rule.  If it succeeds the result is returned,
;;;    otherwise the unchanged expression is returned.
;;; TRANSB1 is the default.
(PUTPROP 'TRANSB (GET 'TRANSB1 'EXPR) 'EXPR)

;;;the pattern matcher. ML is the list of variable bindings necessary to make 
;;;   PAT match E.
(DEFUN INST (E PAT ML) 
  (COND ((EQ ML (QUOTE NO)) ML) 
	((ATOM PAT) 
	  (COND ((ISVAR PAT)
		  ((LAMBDA (W) (COND ((NULL W) (CONS (CONS PAT E) ML))
				     ((EQUAL (CDR W) E) ML) 
				     (T (QUOTE NO)))) 
		   (ASSOC PAT ML)))
		((EQ PAT E) ML) 
		(T (QUOTE NO)))) 
	((ATOM E) (QUOTE NO))
	(T (INST (CDR E) (CDR PAT) (INST (CAR E) (CAR PAT) ML)))))

(DEFUN ISVAR (V) (MEMQ V '(X Y Z)))

(DEFUN SIDE (X Y) X)

;;;Version 1 of rule application an rules

(DEFUN TRANSB1 (E RULE) 
  ((LAMBDA (W) (COND ((EQ W 'NO) E) (T (SUBLIS W (CADR RULE))) ))
   (INST E (CAR RULE) NIL)))

(SETQ R1 '(((PLUS X . Y) (PLUSA X (PLUS . Y)))
	   ((PLUSA 0 . X) (PLUSA . X))
	   ((PLUS) (PLUSB))
	   ((PLUSA X (PLUSB . Y)) (PLUSB X . Y))
	   ((PLUSA (PLUSB . X)) (PLUSB . X))))

(SETQ R2 '(((PLUS X . Y) (PLUSA X (PLUS . Y)))
	   ((PLUS) 0)
	   ((PLUSA 0 . X) (PLUSA . X))
	   ((PLUSA) 0)
	   ((PLUSA X 0) X)
	   ((PLUSA X) X)
	   ((PLUSA (PLUSA X . Y) . Z) (PLUSA X (PLUSA . Y) . Z))
	   ((TIMES X . Y) (TIMESA X (TIMES . Y)))
	   ((TIMES) 1)
	   ((TIMESA 1 . X) (TIMESA . X))
	   ((TIMESA) 1)
	   ((TIMESA X 1) X)
	   ((TIMESA X) X)
	   ((TIMESA (TIMESA X . Y) . Z) (TIMESA X (TIMESA . Y) . Z))
	   ((TIMES 0 . X) 0)
	   ((TIMESA 0 . X) 0)))

;;; Sample run

;;;(PUTPROP TRANSB (GET 'TRANSB1 'EXPR) 'EXPR)

;;;(TRANSFORM '(PLUS A 0) R1 NIL)

;;;(PLUSB A) 
;;;Version 2 of rule application an rules

(DEFUN TRANSB2 (E RULE) 
  ((LAMBDA (W) 
     (COND ((EQ W 'NO) E)
	   ((NOT (EVAL (SUBLIS W (CADR RULE))))  E)
	   ((CADDR RULE) (SUBLIS W ( CADDDR RULE)))
	   (T (EVAL (SUBLIS W (CADDDR RULE)))) ))
   (INST E (CAR RULE) NIL)))

(SETQ R3 '(((PLUS . X) (MEMBER 0 'X) NIL (CONS 'PLUS (DZ 'X)))
	   ((TIMES . X) (MEMBER 0 'X) T 0)
	   ((TIMES . X) (MEMBER 1 'X) NIL (CONS 'TIMES (D1 'X)))
	   ((PLUS) T T 0)
	   ((PLUS X) T T X)
	   ((TIMES) T T 1)
	   ((TIMES X) T T X)))

(DEFUN DZ (U) 
       (COND ((NULL U) NIL)
	     ((EQ (CAR U) 0) (DZ (CDR U)))
	     ((AND (NOT (ATOM (CAR U))) (EQ (CAAR U) 'PLUS))
	      (APPEND (CDAR U) (DZ (CDR U))))
	     (T (CONS (CAR U) (DZ (CDR U))))))

(DEFUN D1 (U) 
       (COND ((NULL U) NIL)
	     ((EQ (CAR U) 1) (D1 (CDR U)))
	     ((AND (NOT (ATOM (CAR U))) (EQ (CAAR U) 'TIMES))
	      (APPEND (CDAR U) (D1 (CDR U))))
	     (T (CONS (CAR U) (D1 (CDR U)))))) 


;;; SAMPLE RUN

;;;(SETQ E1 (DIFF (QUOTE (TIMES X (PLUS Y 1) 3)) (QUOTE X)) )

;;;(PLUS (TIMES 1 (PLUS Y 1) 3) (TIMES X (PLUS 0 0) 3) (TIMES X (PLUS Y 1) 0)) 

;;;(PUTPROP TRANSB (GET 'TRANSB2 'EXPR) 'EXPR)

;;;(TRANSFORM E1 R3 NIL) 
;;;(TIMES (PLUS Y 1) 3)